package reasoner;

//import preprocessor.absorption.extended.ABoxConvertion;
//import utils.exception.ConceptException;
//import java.util.HashMap;
//import java.util.Map;
//
//import preprocessor.absorption.extended.AssertionConversion;

import option.InitParam;
import preprocessor.absorption.extended.AssertionConversion;
import tableaux.Completion;
import utils.Display;
import utils.exception.CoreReasoningException;
import utils.io.KBAccess;
import kb.ABox;
import kb.DescriptionLogicsKB;
import kb.TBox;
import entities.Individual;
import entities.assertion.Assertion;
import entities.assertion.ConceptAssertion;
//import entities.concept.AndConcept;
//import entities.concept.AndConcept;
import entities.concept.Concept;
import entities.concept.NotConcept;
import entities.concept.OrConcept;
import entities.concept.PConcept;
//import entities.concept.PConcept;

/**
 * 
 * This class provides interfaces to the basic operations of the reasoner. Work
 * flow: get the tbox TB by parsing a file/stream: getTBox(String fileName); get
 * the subsumption test concept Con, e.g., A under C?, from a file/stream:
 * getSubsumptionTest(String fileName); call subsumes(Con, TB) to see if Con
 * holds w.r.t. TB. add more axioms: addAxioms(String fileName, TBox tb), to the
 * tbox as you wish, then call subsumes(Con, TB) again!
 * 
 * you don't need to compile the tbox directly, when the subsumption is tested,
 * it will be re-compiled automatically.
 * 
 * @author J.W.Wu
 * 
 */
public class KBReason implements GeneralReason, GuardedReason {
	// private final static boolean ABOX_REASONING = true;
	private static boolean verbose = InitParam.getBooleanProperty("verbose");
	private static boolean showTBox = verbose;
	private static final String reasoner_name = "[C]ARE [A]ssertion [R]etrieval [E]ngine";
	private static final String author_name = "Jiewen Wu";
	private static final String dl_dialect = "SHI(D)";
	private static final String dl_limit = " -- only strings are supported for concrete domain reasoning";
	private static final String author_email = "j55wu@uwaterloo.ca";
	public static final String release_info = "Version: 0.2, Last Compiled: 2013-April-20";
	public static boolean printed = false;

	public static void printReasonerInfo() {
		if (printed) {
			return;
		}
		String sep = "%1$100s";
		System.err.println(String.format(sep, " ").replaceAll(" ", "-"));
		System.err.println(" \t\t\t  " + reasoner_name + " ");
		System.err.println(" A Description Logics Reasoner for " + dl_dialect
				+ ", with the following restrictions:");
		System.err.println(" \t" + dl_limit + ".");
		System.err.println(" \t\tCARE " + release_info + ".");
//		System.err.println(" \tBugs can be reported to " + author_name + " ("
//				+ author_email + ").");
//		System.err.println(" \t\t\t\t\tThanks for using CARE! ");
		System.err.println(String.format(sep, " ").replaceAll(" ", "-"));
		printed = true;
	}

	public KBReason() {
		// default value of verbose
	}

	public KBReason(boolean verbose) {
		KBReason.verbose = verbose;
	}


	public boolean subsumes(Concept c, Concept d, DescriptionLogicsKB kb)
			throws CoreReasoningException {
		KBReason.printReasonerInfo();
		if (Completion.partiallyGuardedReasoning
				|| Completion.fullyGuardedReasoning) {
			return subsumesGuarded(c, d, kb);
		}
		return subsumes(c, d, kb.getTbox(), kb.getAbox());
	}

	private boolean subsumes(Concept c, Concept d, TBox tb, ABox ab)
			throws CoreReasoningException {
		KBReason.printReasonerInfo();
		Individual ind = Individual.getAnonIndividual();
		ConceptAssertion ca = new ConceptAssertion(ind, c);
		ConceptAssertion ast = new ConceptAssertion(ind, d);
		return logicConsequence(ca, ast, tb, ab);
	}

	private ABox getNewAboxByAddingAssertion(ABox old, Assertion ast) {
		ABox newab = null;
		if (old != null) {
			newab = old.deepcopyOfThisABox();
			newab.insertAssertions(ast);
		} else {
			newab = KBAccess.newABoxInstance(ast);
		}
		return newab;
	}

	public boolean logicConsequence(Assertion lhs, Assertion rhs,
			DescriptionLogicsKB kb) throws CoreReasoningException {
		KBReason.printReasonerInfo();
		if (Completion.partiallyGuardedReasoning
				|| Completion.fullyGuardedReasoning) {
			return logicConsequenceGuarded(lhs, rhs, kb);
		}
		if (kb == null) {
			return logicConsequence(lhs, rhs, null, null);
		}
		return logicConsequence(lhs, rhs, kb.getTbox(), kb.getAbox());
	}

	private boolean logicConsequence(Assertion lhs, Assertion rhs, TBox tb,
			ABox ab) throws CoreReasoningException {
		KBReason.printReasonerInfo();
		String s = "\n\n";
		ab.cleanUp();
		ABox rab = null;
		if (lhs != null) {
			rab = getNewAboxByAddingAssertion(ab, lhs);
		} else {
			rab = ab;
		}
		if (tb != null) {
			tb.compileTBox();
		}
		Assertion ast = null;
		if (rhs != null && rhs instanceof ConceptAssertion) {
			s += "Testing if (" + Display.TBOXUNICODE + ", "
					+ Display.ABOXUNICODE + ") " + Display.MODELSUNICODE + " "
					+ rhs.toString();
			ConceptAssertion cast = (ConceptAssertion) rhs;
			// change a:C into a:~C
			ast = new ConceptAssertion(cast.getIndividual(), new NotConcept(
					cast.getConcept()));
		} else {
			throw new CoreReasoningException(
					"Unable to check entailment of a role assertion: "
							+ "reasoner to be updated.");
		}
		Completion dc = new Completion(tb, rab, ast);
		boolean cons = dc.checkABoxConsistency();
		if (!cons) {
			s += "\nGiven assertion is entailed by (T, A).";
		} else {
			s += "\nGiven assertion is NOT entailed by (T, A).";
		}
		if (verbose)
			System.out.println(s);
		return !cons;
	}

	// test if concept c is valid (tautological stmt)
	public boolean subsumesGuarded(Concept c, DescriptionLogicsKB kb)
			throws CoreReasoningException {
		TBox tb = null;
		if (kb != null) {
			tb = AssertionConversion.getConvertedTBox(kb, false);
		}
		Individual ind = Individual.getAnonIndividual();
		ConceptAssertion ast = new ConceptAssertion(ind, new NotConcept(c));
		return logicConsequenceGuarded(null, ast, tb);
	}

	public boolean subsumesGuarded(Concept c, Concept d, DescriptionLogicsKB kb)
			throws CoreReasoningException {
		// OptimizedUniversals.optimize(kb);
		TBox tb = AssertionConversion.getConvertedTBox(kb, false);
		return subsumesGuarded(c, d, tb);
	}

	public boolean subsumesGuarded(Concept c, Concept d, TBox tb)
			throws CoreReasoningException {
		Individual ind = Individual.getAnonIndividual();
		Concept comb = new OrConcept(d, new NotConcept(c));
		ConceptAssertion ast = new ConceptAssertion(ind, comb);
		return logicConsequenceGuarded(null, ast, tb);
	}

	public boolean logicConsequenceGuarded(Assertion lhs, Assertion rhs,
			DescriptionLogicsKB kb) throws CoreReasoningException {
		TBox tb = AssertionConversion.getConvertedTBox(kb, false);
		return logicConsequenceGuarded(lhs, rhs, tb);
	}

	public static long nomsize = 0;
	public static long numinf = 0;


	// assuming tb is already normalized
	public boolean logicConsequenceGuarded(Assertion lhs, Assertion rhs, TBox tb)
			throws CoreReasoningException {
		KBReason.printReasonerInfo();
		nomsize += Individual.resetAllIndividuals();
		numinf++;
		String s = "\n";
		// if(lhs.asConceptAssertion().getIndividual().getName().contains("canon_eos5d_1")){
		// System.out.println("Debugging");
		// }
		if (lhs != null) {
			if (lhs instanceof ConceptAssertion
					&& rhs instanceof ConceptAssertion) {
				if (!lhs.asConceptAssertion().getIndividual()
						.equals(rhs.asConceptAssertion().getIndividual())) {
					throw new CoreReasoningException(
							"LHS and RHS concept assertions must be of the same instance.");
				}
				Concept lc = lhs.asConceptAssertion().getConcept(), rc = rhs
						.asConceptAssertion().getConcept();
				Concept nc = null;
				if (!lc.isTop()) {
					nc = new OrConcept(new NotConcept(lc), rc);
				} else {
					nc = rc;
				}
				rhs = new ConceptAssertion(lhs.asConceptAssertion()
						.getIndividual(), nc);
			} else {
				throw new CoreReasoningException(
						"No support for update in queries. "
								+ "Unable to check entailment of a role assertion");
			}
		}
		if (tb != null) {
			tb.compileTBox();
			if (showTBox) {
				System.out
						.println("\nAfter absorption\nConverted Tbox binary entries: "
								+ tb.getSpecialBinaryClass()
										.getNumberOfEntries());
				System.out.println("Binary entries hash table size: "
						+ tb.getSpecialBinaryClass().getTbLimited().size());
				System.out.println("Unary entries: " + tb.getTu().size());
				System.out.println("GCIs: " + tb.getTg());
				// FileLoader.writeAsFile(tb.getTg().toString(), "GCIs.txt",
				// ", ");
				System.out.println("Newly introduced internal concepts: "
						+ PConcept.getNumFrenshConcept());
				System.out.println("Newly introduced guarded concepts: "
						+ PConcept.getGuardedConcept().size());
				showTBox = false;
			}
		}
		Assertion ast = null;
		if (rhs != null && rhs instanceof ConceptAssertion) {
			s += "Testing if " + Display.TBOXUNICODE + Display.MODELSUNICODE
					+ " " + rhs.toString() + " is entailed by KB: ";
			// System.err.println(s);
			ConceptAssertion cast = (ConceptAssertion) rhs;
			ast = new ConceptAssertion(cast.getIndividual(), new NotConcept(
					cast.getConcept()));
		} else {
			throw new CoreReasoningException(
					"Unable to check entailment of a role assertion: "
							+ "reasoner to be updated.");
		}
		Completion dc = new Completion(tb, null, ast);
		// System.err.println("assertion: "+ast);
		boolean cons = dc.checkABoxConsistency();
		// dc.getRelatedInstances();
		if (!cons) {
			s += "YES";
		} else {
			s += "NO";
		}
		if (verbose)
			System.out.println(s);
		return !cons;
	}

}
